\section{Matematyka konstruktywistyczna} \label{sec:matematyka-konstruktywistyczna}
Matematyka konstruktywistyczna to matematyka w której ``jedyny sposób pokazania że obiekt istnienie to przedstawienie sposobu znalezienia go w skończonej liczbie kroków.'' (cytat: Erret Bishop \cite{bishop})

Matematyka konstruktywistyczna różni się od matematyki klasycznej interpretacją kwantyfikatorów oraz spójników logicznych \cite[rozdział 2]{sep-mathematics-constructive}:
\begin{center}
\begin{longtable}{l | l}
  \(A \lor B \) & Należy przedstawić dowód \(A\) lub przedstawić dowód \(B\) \\
  \(A \land B \) & Należy przedstawić dowód \(A\) i przedstawić dowód \(B\) \\
  \(A \implies B \) & Należy przedstawić sposób przerobienia dowodu \(A\) na dowód \(B\) \\ 
  \( \neg A \) & Należy udowodnić że \( A \implies  \bot \)\footnote{$\bot$ to \emph{absurd} (opisany w : (\ref{subsec:absurd}))} \\
  \( \exists x : P(x) \) & Należy skonstruować $x$ i przedstawić dowód $P(x)$ \\
  \( \forall x \in S : P(x) \) & Należy przedstawić procedurę, która dla dowolnego obiektu $x$ dowodzi \( x \in S \implies P(x) \)
\end{longtable}
\end{center}
%W praktyce sprowadza się to do odrzucenia prawa wyłączonego środka (jak opisano w (\ref{sec:niekonstruktywnost}))

\subsection{Dowód nieistnienia (absurd)} \label{subsec:absurd}
Aby udowodnić \(\neg P\), sprowadza się $P$ do absurdu, oznaczanego jako $\bot$ lub $\mathbf{0}$. \emph{Absurd} jest zdaniem fałszywym z definicji. W teorii typów {\PerMartinLofDopelniacz} absurd to typ, który z definicji nie może mieć instancji, analogicznie do następującej klasy w języku Java:
\begin{verbatim}
class Empty {
  private Empty() {
  }
}
\end{verbatim}
Przykład użycia:
\begin{theorem}
  Niech liczby naturalne będą zdefiniowane przez postulaty Peano, a za absurd przyjmuje się $0 = 1$. Wtedy:
  \[ \neg (1 = 2) \]
\end{theorem} 
\begin{proof}
  Niech $p$ będzie dowodem że \(1 = 2 \).
  $1$ nie jest zerem oraz $2$ nie jest zerem, a zatem obie strony równania są w dziedzinie operacji poprzednika.
  Przykładam operację poprzednika do obu stron $p$, otrzymując \(0 = 1 \).
\end{proof}
